$\forall$${\it es}$:ES, ${\it ff}$:FIFO, $p$:(E$\rightarrow\mathbb{P}$), $e$:E, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C.
\\[0ex]($\forall$$e$:E. Dec($p$($e$))) $\Rightarrow$ ($\forall$$e$:E. Dec(${\it ff}$.S(${\it sndr}$,${\it rcvr}$,$e$))) $\Rightarrow$ Dec([$e$: ${\it sndr}$ $--$$p$$\rightarrow$ ${\it rcvr}$])